/LMAR=0/XLINE=4/FONT#0=BASL30/FONT#1=BASB30/FONT#5=ASI30[LSP,JRA]/FONT#2=ASI30[LSP,JRA]/FONT#3=SUB/FONT#4=SET1/FONT#6=GRK30/FONT#7=SUP/FONT#8=SPEC[LSP,JRA]/FONT#9=BUCK75/FONT#10=GRFX25[LSP,JRA]/FONT#11=METSB/FONT#12=NGB30/FONT#13=GERM35/FONT#14=MG[LSP,JRA]/FONT#15=GRFX35
␈↓ α←␈↓␈↓␈↓ 	≡CONTENTS     i␈↓

␈↓"β␈↓ α←␈↓↓␈↓ ∧aT A B L E   O F   C O N T E N T S



␈↓"β␈↓ α←␈↓␈↓↓PREFACE␈↓ 
Ei␈↓

␈↓"β␈↓ α←␈↓␈↓↓CHAPTER␈↓ 	|PAGE␈↓


␈↓"β␈↓ α←␈↓␈↓ ββ1␈↓ β3SYMBOLIC EXPRESSIONS␈↓ 
@1

␈↓"β␈↓ α←␈↓␈↓ βc1.1␈↓ ∧+Introduction␈↓ ¬G .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  . ␈↓ 
6 1


␈↓"β␈↓ α←␈↓␈↓↓INDEX␈↓ 
Fi␈↓
␈↓ α←␈↓␈↓1.␈↓ λ⊃Symbolic expressions     1␈↓




␈↓"β␈↓ α←␈↓␈↓ 	"␈↓↓CHAPTER 1␈↓




␈↓"β␈↓ α←␈↓␈↓	Symbolic Expressions␈↓














␈↓"β␈↓ α←␈↓␈↓ ¬h␈↓↓1.1  Introduction␈↓

␈↓"β␈↓ α←␈↓With this introduction, here is ␈↓αcomplis␈↓ and friends:
␈↓"∀␈↓ α←␈↓␈↓αcomplis <= λ[[u;off;vpl] complis␈↓λ'␈↓α[u;off;off;vpl;();();();1]␈↓
␈↓"∀␈↓ α←␈↓αcomplis␈↓λ'␈↓α <= λ[[u;org;off;vpl;triv;cmplx;pop;ac]
␈↓"β␈↓ α←␈↓α␈↓ ∧∪[null[u] →␈↓ ¬↔[null[cmplx] → triv;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔ ␈↓
t␈↓α → append␈↓ ε3[rest[cmplx];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε3 list[mkmove[mem[first[pop]];1]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε3 rest[pop];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε3 triv]];
␈↓"	␈↓ α←␈↓α␈↓ ∧∪ isconst[first[u]] → complis␈↓λ'␈↓α[␈↓ ε{rest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{org;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{off;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{vpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{concat[mkconst[ac;first[u]];triv];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{cmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{pop;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{add1[ac]];
␈↓ α←␈↓␈↓2  Symbolic expressions␈↓ 
(1.1␈↓

␈↓"	␈↓ α←␈↓α␈↓ ∧∪ isvar[first[u]] → complis␈↓λ'␈↓α[␈↓ εcrest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcorg;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcoff;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcvpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcconcat[␈↓ π7mkvar[␈↓ λac;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εc␈↓ π7␈↓ λloc[first[u];off;vpl]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εc␈↓ π7triv];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εccmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcpop;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcadd1[ac]];
␈↓"	␈↓ α←␈↓α␈↓ ∧∪ iscarcdr[first[u]] → complis␈↓λ'␈↓α[␈↓ ππrest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππorg;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππoff;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππvpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππappend[␈↓ πsreverse[compcarcdr[␈↓ 	cac;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππ␈↓ πs␈↓ 	c first[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππ␈↓ πs␈↓ 	c off;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππ␈↓ πs␈↓ 	c vpl]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππ␈↓ πstriv];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππcmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππpop;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππadd1[ac]];
␈↓"	␈↓ α←␈↓α␈↓ ∧∪ iscond[first[u] → complis␈↓λ'␈↓α[␈↓ εorest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εoorg;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εosub1[off];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εovpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εotriv;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εoappend[␈↓ π[cmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[concat[␈↓ λ/mkpush[1];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[␈↓ λ/comcond[␈↓ 	≠args␈↓βc␈↓α[␈↓ 	cfirst[u]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[␈↓ λ/␈↓ 	≠gensym[];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[␈↓ λ/␈↓ 	≠off;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[␈↓ λ/␈↓ 	≠vpl]]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εoconcat[mkpop[ac];pop];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εoadd1[ac]];
␈↓ α←␈↓␈↓1.1␈↓ λ|Introduction     3␈↓

␈↓"	␈↓ α←␈↓α␈↓ ∧∪ ␈↓
t␈↓α → complis␈↓λ'␈↓α[␈↓ ¬Grest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gorg;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gsub1[off];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gvpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gtriv;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gappend[␈↓ ε3cmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3concat[␈↓ ππmkpush[1];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππλ[[z] compapply[␈↓ λ←func[first[u]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ␈↓ λ←complis[␈↓ 	Kz;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ␈↓ λ←␈↓ 	Koff;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ␈↓ λ←␈↓ 	Kvpl];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ␈↓ λ←length[z]]]
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ [arglist[first[u]] ]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gconcat[mkpop[ac];pop];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gadd1[ac]]]
␈↓"→␈↓ α←␈↓αmkmove <= λ[[ac;loc][eq[ac;loc] → (); ␈↓
t␈↓α → list[MOVE;ac;loc]]]
␈↓"∀␈↓ α←␈↓αcompcarcdr <= λ[[ac;exp;off;vpl]
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7[isvar[arg[exp]] → list[mkcarcdr[␈↓ π[func[exp];
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7␈↓ ¬G␈↓ π[ac;
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7␈↓ ¬G␈↓ π[loc[arg[exp];off;vpl]]]
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7␈↓
t␈↓α → concat[␈↓ ¬Gmkcarcdr_ac[func[exp];ac;ac];
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7␈↓ ¬Gcompcarcdr[ac;arg[exp];off;vpl]]]]
␈↓"∀␈↓ α←␈↓αiscarcdr <=λ[[u]␈↓ ∧7[iscar[u] →iscarcdr[arg[u]]
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7 iscdr[u] →iscarcdr[arg[u]]
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7 atom[u] → or[isvar[u];isconst[u]];
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7 ␈↓
t␈↓α → ␈↓
f␈↓α ]]
␈↓"∀␈↓ α←␈↓αiscar <= λ[[x] eq[func[x];CAR]]
␈↓"	␈↓ α←␈↓αiscdr <= λ[[x] eq[func[x];CDR]]
␈↓"	␈↓ α←␈↓αmkcarcdr <=λ[[carcdr;ac;loc] list[carcdr;ac;loc]]
␈↓ α←␈↓␈↓␈↓ 	KINDEX     5␈↓









␈↓ α←␈↓␈↓	Index␈↓